1 Contenido de la clase
Repaso: la función de Ackermann y sus propiedades [00:00-06:50]
La clase empieza retomando la función de Ackermann y sus propiedades, demostradas por inducción: A(1, z) = z + 2, A(2, z) = 2z + 3, A(3, z) = 2^(z+3) − 3, y A(4, z) con torres de exponentes de 2 [06:54-07:00, 25:12-25:26]. Se muestran valores enormes: A(4, 1) = 65533 y A(4, 2) tiene 19 729 dígitos; A(5, 2) ni siquiera cabría en el universo físico [03:13-03:54]. Se usan inducción sobre una variable y doble inducción (sobre dos variables) para demostrarlas [64:20-64:54]. [parte no entendida — partes del desarrollo en la pizarra].
Verificación de programas y problemas no computables [65:12-69:14]
Se cierra el tema de la verificación: saber si un programa es correcto es, en general, un problema sin solución; no existe un sistema que acepte los programas correctos y rechace los incorrectos [65:14-65:40]. El Teorema de la Incompletitud de Gödel establece que el sistema falla en detectar la corrección: existen programas de los que no se puede saber si son correctos [65:42-65:56]. En un sistema formal con axiomas que no se contradicen hay enunciados que no se pueden probar ni refutar [65:58-66:16]. Sistemas formales: aritmética, lógica, geometría [66:18-66:52]. El teorema aplica cuando el sistema es recursivo (la deducción se lleva a cabo mediante un algoritmo) [67:00-67:18].
La demostración con ciclos asume que el ciclo termina [67:31-68:05]
La demostración de programas con ciclos (inducción e invariantes) asume que el ciclo termina. Por eso conviene saber si el ciclo termina, y decidir si un programa termina es no computable [67:31-68:14]. Si el programa termina, la corrección total está garantizada; si no, no se puede afirmar [68:18-68:27].
El problema del paro (halting problem) [01:53-09:15]
Se demuestra que no existe un algoritmo para determinar si un programa termina, por reducción al absurdo con la técnica de diagonalización: se supone que existe SeDetiene(P, D), se define SePara(P) = indefinido si SeDetiene(P, P), definido si no [02:43-03:34], se compone SeDetiene(SePara, P) y se evalúa el caso P = SePara [04:31-06:51]. La composición lleva a una contradicción: SeDetiene(SePara, SePara) sería a la vez cierto y falso [06:51-09:01]. Como todo lo construido era correcto, la contradicción viene de suponer que SeDetiene existe, por lo que no existe tal algoritmo [09:05-09:15]. El problema es parcialmente computable: si el programa realmente se detiene, ejecutarlo lo muestra; pero en general no se puede saber (p. ej. cuadros mágicos que tardan días) [09:15-20:11].
Otros problemas no computables [68:45-69:11]
Otros ejemplos: el problema de la equivalencia (determinar si dos programas hacen lo mismo), el Teorema de Rice (no existe un algoritmo que indique si un programa arbitrario realizará determinada tarea), decidir si dos gramáticas representan el mismo lenguaje, y decidir si una gramática independiente del contexto es ambigua (permite dos interpretaciones distintas) — todos sin solución [68:45-69:11].
Programación Lógica: introducción e historia [24:06-27:10]
Se motiva la Programación Lógica como una herramienta o lenguaje auxiliar para resolver ciertos problemas (sobre todo de inteligencia artificial: representación de conocimiento, deducción, bases de datos) [24:06-25:08, 25:55-26:14]. En 1879, Gottlob Frege publica el cálculo de predicados (lógica de primer orden). En los años 30, Herbrand, Skolem y Gödel demuestran que toda fórmula válida tiene una prueba formal construible de manera sistemática, es decir, existe un algoritmo. En 1965, John Alan Robinson propone la regla de resolución para la demostración automática. En 1971, en la Universidad de Marsella, el grupo de Alain Colmerauer crea PROLOG (PROgrammation LOGique), establecido formalmente como lenguaje por Robert Kowalski [Nota 8, págs. 11-13]. Existen otros lenguajes lógicos (ALF, Gödel, Mercury, Lambda Prolog) e intentos de añadir orientación a objetos y paralelismo [Nota 8, pág. 14].
Lógica de primer orden: elementos del lenguaje [Nota 8, págs. 14-19]
Los elementos son: constantes (minúsculas: 1, a, pedro), variables (inicial mayúscula: X, Nombre), funciones (minúsculas: numero(par)), términos (constante, variable o f(t1,…,tn)), predicados (expresan relaciones y tienen valor de verdad: numero(X), da(regalo, juan, maria)), conectivos lógicos (conjunción ∧, disyunción ∨, negación ¬, implicación →, equivalencia ↔) y cuantificadores (∃ existencial, ∀ universal). Una fórmula es un predicado o se construye combinando fórmulas con conectivos y cuantificadores [Nota 8, págs. 14-18].
Cláusulas de Horn y resolución [Nota 8, págs. 19-22]
Una cláusula es una disyunción de literales cuantificada universalmente; las cláusulas de Horn tienen a lo sumo una literal no negada y son con las que trabaja Prolog [Nota 8, pág. 19]. Se reescriben como: hechos (L1.), reglas (L1 :- L2, …, Lm.) y metas (?- L2, …, Lm.) [Nota 8, pág. 20]. La resolución aplicada a estas fórmulas deduce nuevas metas; al llegar a la cláusula vacía, la meta es verdadera [Nota 8, págs. 20-22]. En las metas `←` se sustituye por `?-`, en las reglas por `:-`, y en los hechos se elimina; todo termina con punto [Nota 8, pág. 24].
2 Puntos destacados / Lo que hay que saber
SeDetiene(P,D); se demuestra por diagonalización (contradicción al componer SeDetiene y SePara) [01:53-09:15].:-) y metas (?-) [Nota 8].3 Actividades y tareas pendientes
4 Dudas que podrían examinar
¿Por qué no se puede saber si un programa es correcto?
Por el Teorema de Incompletitud de Gödel: en todo sistema formal recursivo hay enunciados que no se pueden probar ni refutar; análogamente, hay programas cuya corrección no se puede decidir [65:42-66:16].
¿Qué es el problema del paro?
Determinar si un programa termina (o no) es no computable: no existe un algoritmo SeDetiene(P,D) [01:53-02:06, 68:08-68:14].
¿Cómo se demuestra que el problema del paro no es computable?
Por reducción al absurdo y diagonalización: se supone que existe SeDetiene, se define SePara y al componerlas con P = SePara se llega a una contradicción [02:43-09:15].
¿Qué es el Teorema de Rice?
No existe un algoritmo que indique si un programa arbitrario realizará o no determinada tarea [68:50-68:53].
¿Qué es una gramática ambigua?
Una gramática independiente del contexto que permite dos interpretaciones distintas; decidir si lo es, es no computable [69:03-69:11].
¿Qué es la Programación Lógica?
Un paradigma que usa la lógica de primer orden como base de programación, con lenguajes como PROLOG [24:06-24:16].
¿Qué es la resolución?
Regla de inferencia propuesta por Robinson (1965) para demostración automática: de P ∨ Q y ¬Q se concluye P; aplicada a cláusulas de Horn deduce metas hasta la cláusula vacía [Nota 8].
¿Qué es una cláusula de Horn?
Una cláusula con a lo sumo una literal no negada; en Prolog se escribe como hecho, regla (:-) o meta (?-) [Nota 8].
5 Sitios o recursos para visitar
Por qué en todo sistema formal recursivo hay enunciados indecidibles. · es.wikipedia.org
El problema del paro y su demostración por diagonalización. · es.wikipedia.org
Propiedades no triviales de los programas que no se pueden decidir. · es.wikipedia.org
El paradigma que usa la lógica de primer orden como base de programación. · es.wikipedia.org
Las cláusulas con a lo sumo una literal no negada que usa Prolog. · es.wikipedia.org
La regla de inferencia de Robinson para demostración automática. · es.wikipedia.org
El lenguaje representativo de la programación lógica. · es.wikipedia.org
6 Glosario de términos
- Problema no computable: problema para el que no existe un algoritmo que lo resuelva.
- Sistema formal: lenguaje + gramática formal + axiomas + reglas de inferencia; ej. aritmética, lógica, geometría.
- Teorema de incompletitud de Gödel: en todo sistema formal recursivo consistente existen enunciados no demostrables ni refutables.
- Problema del paro (halting): decidir si un programa termina; es no computable.
- Diagonalización: técnica de demostración que usa un valor en la diagonal (P con P) para exhibir una contradicción.
- Teorema de Rice: no existe algoritmo que decida propiedades no triviales de los programas.
- Gramática ambigua: gramática independiente del contexto que permite dos interpretaciones distintas.
- Programación Lógica: paradigma que usa la lógica de primer orden como base de programación.
- Cálculo de predicados: lógica de primer orden (Frege, 1879).
- Resolución: regla de inferencia para demostración automática (Robinson, 1965).
- Cláusula: disyunción de literales cuantificada universalmente.
- Cláusula de Horn: cláusula con a lo sumo una literal no negada; la que usa Prolog.
- Hecho, regla y meta: en Prolog, cláusulas de Horn escritas como
L1.,L1 :- L2, …, Lm.y?- L2, …, Lm.. - Literal: fórmula atómica o su negación.
- Fórmula atómica: predicado, fórmula sin conectivos ni cuantificadores.
- Término: constante, variable o función aplicada a términos.
7 Mapa mental textual
- Problemas no computables y Programación Lógica · Clase 8
- Verificación de programas
- Saber si un programa es correcto es no computable
- Teorema de incompletitud de Gödel (sistema formal recursivo)
- Demostración con ciclos asume que el ciclo termina
- Problema del paro
- No existe algoritmo SeDetiene(P,D)
- Demostración por diagonalización (SePara + contradicción)
- Parcialmente computable
- Otros no computables
- Equivalencia de programas · Teorema de Rice · gramática ambigua
- Función de Ackermann (repaso)
- A(1,z)=z+2, A(2,z)=2z+3, A(3,z)=2^(z+3)−3
- A(4,1)=65533, A(4,2) con 19729 dígitos
- Programación Lógica
- Historia: Frege (1879) → Herbrand/Skolem/Gödel (30s) → Robinson/resolución (1965) → PROLOG (1971)
- Lógica de primer orden: constantes, variables, funciones, términos, predicados, conectivos, cuantificadores
- Cláusulas de Horn: hechos, reglas (
:-), metas (?-) - Resolución: deducir metas hasta la cláusula vacía
- Verificación de programas